We study the problem of training and certifying adversarially robust quantized neural networks (QNNs). Quantization is a technique for making neural networks more efficient by running them using low-bit integer arithmetic and is therefore commonly adopted in industry. Recent work has shown that floating-point neural networks that have been verified to be robust can become vulnerable to adversarial attacks after quantization, and certification of the quantized representation is necessary to guarantee robustness. In this work, we present quantization-aware interval bound propagation (QA-IBP), a novel method for training robust QNNs. Inspired by advances in robust learning of non-quantized networks, our training algorithm computes the gradient of an abstract representation of the actual network. Unlike existing approaches, our method can handle the discrete semantics of QNNs. Based on QA-IBP, we also develop a complete verification procedure for verifying the adversarial robustness of QNNs, which is guaranteed to terminate and produce a correct answer. Compared to existing approaches, the key advantage of our verification procedure is that it runs entirely on GPU or other accelerator devices. We demonstrate experimentally that our approach significantly outperforms existing methods and establish the new state-of-the-art for training and certifying the robustness of QNNs.

We study the problem of learning controllers for discrete-time non-linear stochastic dynamical systems with formal reach-avoid guarantees. This work presents the first method for providing formal reach-avoid guarantees, which combine and generalize stability and safety guarantees, with a tolerable probability threshold $p\in[0,1]$ over the infinite time horizon. Our method leverages advances in machine learning literature and it represents formal certificates as neural networks. In particular, we learn a certificate in the form of a reach-avoid supermartingale (RASM), a novel notion that we introduce in this work. Our RASMs provide reachability and avoidance guarantees by imposing constraints on what can be viewed as a stochastic extension of level sets of Lyapunov functions for deterministic systems. Our approach solves several important problems -- it can be used to learn a control policy from scratch, to verify a reach-avoid specification for a fixed control policy, or to fine-tune a pre-trained policy if it does not satisfy the reach-avoid specification. We validate our approach on $3$ stochastic non-linear reinforcement learning tasks.

我们考虑在离散时间非线性随机控制系统中正式验证几乎核实（A.S.）渐近稳定性的问题。在文献中广泛研究确定性控制系统中的验证稳定性，验证随机控制系统中的验证稳定性是一个开放的问题。本主题的少数现有的作品只考虑专门的瞬间形式，或对系统进行限制性假设，使其无法与神经网络策略的学习算法不适用。在这项工作中，我们提出了一种具有两种新颖方面的一般非线性随机控制问题的方法：（a）Lyapunov函数的经典随机扩展，我们使用排名超大地区（RSMS）来证明〜渐近稳定性，以及（B）我们提出一种学习神经网络RSM的方法。我们证明我们的方法保证了系统的渐近稳定性，并提供了第一种方法来获得稳定时间的界限，其中随机Lyapunov功能不。最后，我们在通过神经网络政策的一套非线性随机强化学习环境上通过实验验证我们的方法。

贝叶斯神经网络（BNNS）将分布放在神经网络的重量上，以模拟数据的不确定性和网络的预测。我们考虑在具有无限时间地平线系统的反馈循环中运行贝叶斯神经网络策略时验证安全的问题。与现有的基于样品的方法相比，这是不可用的无限时间地平线设置，我们训练一个单独的确定性神经网络，用作无限时间的地平线安全证书。特别是，我们证明证书网络保证了系统的安全性在BNN重量后部的子集上。我们的方法首先计算安全重量，然后改变BNN的重量后，以拒绝在该组外的样品。此外，我们展示了如何将我们的方法扩展到安全探索的强化学习环境，以避免在培训政策期间的不安全轨迹。我们在一系列加固学习基准上评估了我们的方法，包括非Lyapunovian安全规范。

我们介绍了一种新的随机验证算法，该算法正式地定量了配制成连续深度模型的任何连续过程的行为稳健性。我们的算法在给定的时间范围内解决了一组全局优化（GO）问题，以构造从初始状态的球开始的所有处理执行集的紧密机箱（管）。我们称我们的算法GoTube。通过其结构，GoTube确保边界管保守达到所需的概率和最高的紧密性。 GoTube以JAX实现，并优化以扩展到复杂的连续深度神经网络模型。与用于时间持续神经网络的高级可达性分析工具相比，GoTube不会在时间步骤之间积累过度估计误差，并避免符号技术中固有的臭名昭着包装效果。我们展示了GOTUBE在初始球，速度，时间 - 地平线，任务完成和大量实验中的可扩展性方面表现出最先进的验证工具。 GOTUBE是稳定的，并在其能够扩展到以前可能的视野的能力方面来设置最先进的。

当预测它们被训练以识别时的输入类时，神经网络分类器可以实现高精度。在动态环境中保持这种准确性，其中输入经常掉落在最初已知的类的固定集合之外，仍然是一个挑战。典型方法是检测新颖类别的输入，并在增强的数据集上重新转回分类器。但是，不仅是分类器还是检测机制也需要适应以区分新学习和尚未未知的输入类。为了解决这一挑战，我们介绍了一个算法框架，用于神经网络的主动监控。在我们的框架中包装的监视器与神经网络并行运行，并通过一系列可解释的标记查询与人类用户进行交互，以增量适应。此外，我们提出了一种自适应定量监测，以提高精度。具有不同数量的类别的多种基准测试的实验评估证实了我们在动态方案中的主动监测框架的好处。

Edge computing is changing the face of many industries and services. Common edge computing models offload computing which is prone to security risks and privacy violation. However, advances in deep learning enabled Internet of Things (IoTs) to take decisions and run cognitive tasks locally. This research introduces a decentralized-control edge model where most computation and decisions are moved to the IoT level. The model aims at decreasing communication to the edge which in return enhances efficiency and decreases latency. The model also avoids data transfer which raises security and privacy risks. To examine the model, we developed SAFEMYRIDES, a scene-aware ridesharing monitoring system where smart phones are detecting violations at the runtime. Current real-time monitoring systems are costly and require continuous network connectivity. The system uses optimized deep learning that run locally on IoTs to detect violations in ridesharing and record violation incidences. The system would enhance safety and security in ridesharing without violating privacy.

Cognitive Computing (COC) aims to build highly cognitive machines with low computational resources that respond in real-time. However, scholarly literature shows varying research areas and various interpretations of COC. This calls for a cohesive architecture that delineates the nature of COC. We argue that if Herbert Simon considered the design science is the science of artificial, cognitive systems are the products of cognitive science or 'the newest science of the artificial'. Therefore, building a conceptual basis for COC is an essential step into prospective cognitive computing-based systems. This paper proposes an architecture of COC through analyzing the literature on COC using a myriad of statistical analysis methods. Then, we compare the statistical analysis results with previous qualitative analysis results to confirm our findings. The study also comprehensively surveys the recent research on COC to identify the state of the art and connect the advances in varied research disciplines in COC. The study found that there are three underlaying computing paradigms, Von-Neuman, Neuromorphic Engineering and Quantum Computing, that comprehensively complement the structure of cognitive computation. The research discuss possible applications and open research directions under the COC umbrella.

When testing conditions differ from those represented in training data, so-called out-of-distribution (OOD) inputs can mar the reliability of black-box learned components in the modern robot autonomy stack. Therefore, coping with OOD data is an important challenge on the path towards trustworthy learning-enabled open-world autonomy. In this paper, we aim to demystify the topic of OOD data and its associated challenges in the context of data-driven robotic systems, drawing connections to emerging paradigms in the ML community that study the effect of OOD data on learned models in isolation. We argue that as roboticists, we should reason about the overall system-level competence of a robot as it performs tasks in OOD conditions. We highlight key research questions around this system-level view of OOD problems to guide future research toward safe and reliable learning-enabled autonomy.

Rigorous guarantees about the performance of predictive algorithms are necessary in order to ensure their responsible use. Previous work has largely focused on bounding the expected loss of a predictor, but this is not sufficient in many risk-sensitive applications where the distribution of errors is important. In this work, we propose a flexible framework to produce a family of bounds on quantiles of the loss distribution incurred by a predictor. Our method takes advantage of the order statistics of the observed loss values rather than relying on the sample mean alone. We show that a quantile is an informative way of quantifying predictive performance, and that our framework applies to a variety of quantile-based metrics, each targeting important subsets of the data distribution. We analyze the theoretical properties of our proposed method and demonstrate its ability to rigorously control loss quantiles on several real-world datasets.